inv-rel(A;B;f;finv)
== (a:A, b:B. (finv(b) = (inl a ))  (b = f(a))) & (a:A. finv(f(a)) = (inl a )) 

latex

---

clarification:

inv-rel(A;B;f;finv)
== (a:A, b:B. (finv(b) = (inl a )  (A + Unit))  (b = f(a)  B))
== & (a:A. finv(f(a)) = (inl a )  (A + Unit)) 

latex

Definitions	P & Q, P  Q, x:A. B(x), s = t, left + right, Unit, f(a), inl x
FDL editor aliases	inv-rel